(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(x1) → b(x1)
b(b(b(c(x1)))) → c(c(a(a(b(a(x1))))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(a(b(a(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(a(b(a(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
B(
b(
b(
c(
z0)))) →
c2(
A(
a(
b(
a(
z0)))),
A(
b(
a(
z0))),
B(
a(
z0)),
A(
z0)) by
B(b(b(c(x0)))) → c2(A(b(b(a(x0)))), A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(x0)))) → c2(A(b(b(a(x0)))), A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(x0)))) → c2(A(b(b(a(x0)))), A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
B(
b(
b(
c(
x0)))) →
c2(
A(
b(
b(
a(
x0)))),
A(
b(
a(
x0))),
B(
a(
x0)),
A(
x0)) by
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(a(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c2
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
B(
b(
b(
c(
z0)))) →
c2(
A(
a(
b(
b(
z0)))),
A(
b(
a(
z0))),
B(
a(
z0)),
A(
z0)) by
B(b(b(c(x0)))) → c2(A(b(b(b(x0)))), A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c2, c2
(9) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0)) by B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(x0)))) → c2(A(b(a(x0))))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c2, c2
(11) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace B(b(b(c(x0)))) → c2(A(b(a(x0)))) by B(b(b(c(z0)))) → c2(A(b(b(z0))))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(a(z0)), A(z0))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c2, c2
(13) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace B(b(b(c(x0)))) → c2(A(b(b(b(x0)))), A(b(a(x0))), B(a(x0)), A(x0)) by B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c2, c2
(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
A(
z0) →
c1(
B(
z0)) by
A(b(b(c(b(c(y0)))))) → c1(B(b(b(c(b(c(y0)))))))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
A(b(b(c(b(c(y0)))))) → c1(B(b(b(c(b(c(y0)))))))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))
S tuples:
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
A(b(b(c(b(c(y0)))))) → c1(B(b(b(c(b(c(y0)))))))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
B, A
Compound Symbols:
c2, c2, c2, c1
(17) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
B(b(b(c(b(c(z0)))))) → c2(A(a(c(c(a(a(b(a(z0)))))))), A(b(a(b(c(z0))))), B(a(b(c(z0)))), A(b(c(z0))))
B(b(b(c(b(b(c(z0))))))) → c2(A(a(b(c(c(a(a(b(a(z0))))))))), A(b(a(b(b(c(z0)))))), B(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(A(b(a(x0))), B(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(b(b(b(z0)))), A(b(a(z0))), B(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(b(b(z0))))
A(b(b(c(b(c(y0)))))) → c1(B(b(b(c(b(c(y0)))))))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → c(c(a(a(b(a(z0))))))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:none
Compound Symbols:none
(19) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(20) BOUNDS(O(1), O(1))